x, y:Atom1. x =a1 y  x  y 

latex

Definitions	P  Q, P & Q, x:AB(x), P  Q, P  Q, x:AB(x), A, b, eq_atom$n(x;y), Prop, s = t, a  b, x:A. B(x), t  T, Atom$n
Lemmas	nequal wf, eq atom wf1, assert wf, not wf, assert of eq atom1, not functionality wrt iff, iff functionality wrt iff